\begin{tabbing}
ecl{-}machine at $i$ with state \$ecl
\\[0ex]
\\[0ex]$A$
\\[0ex]
\\[0ex]state variables ${\it ds}$
\\[0ex]
\\[0ex]actions ${\it da}$
\\[0ex]
\\[0ex]sends ${\it snd}$
\\[0ex]
\\[0ex]updates ${\it upd}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=ecl{-}machine1\=\{\$ecl:ut2\}\+\+
\\[0ex]($i$; ${\it ds}$; ${\it da}$; $A$)
\-\\[0ex]$\oplus$ \=let $T$,${\it ks}$,${\it init}$,${\it tr}$,$h$,$a$,${\it es}$ = ecl{-}trans($A$) in \+
\\[0ex]ecl{-}machine2($i$;${\it ds}$;${\it da}$;"\$ecl";$T$;${\it ks}$;$a$;${\it upd}$) $\oplus$ ecl{-}machine3(${\it ds}$;${\it da}$;"\$ecl";$T$;${\it ks}$;$a$;${\it snd}$)
\-\-
\end{tabbing}